COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Proving facts about programs that order ordinals
C00003 ENDMK
C⊗;
Proving facts about programs that order ordinals

Let the ordinals less than epsilon zero be represented as numbers
and lists.  An ordinal is either a number or a list of ordinals
in descending order.  Write programs as follows:

1. To test whether an S-expression represents and ordinal.

2. To compare two ordinals.

Make proofs as follows:

1. Prove that the above written programs are total.

2. Prove trichotomy.

3. Prove transitivity.

Write a schema expressing the fact that the ordering is a well-ordering.

Can you prove it?